1. Field
The present invention relates to modeling and testing digital designs of state machines, and more specifically, to systems, methods and computer products for the identification of dependent state variables to aid in logic design and verification.
2. Background
A system such as an electrical circuit including state holding elements may be modeled using state equations and state variables that describe the behavior and state of the system. A complete set of state variables for a system typically contains enough information about the system's history to enable computation of the system's future behavior. Simplifying the model to reduce the number of state variables lessens the computational cost of analyzing the model, for example, to verify that it conforms to a given specification.
Dependent state element identification refers to the process of identifying those state variables in a design (e.g. latches or registers) that can be expressed as combinational (Boolean) functions of other state variables. A special case of dependent state variables are redundant state variables, in which two registers evaluate to the same value at all points in time. For example, one register may be expressible as a function of other registries, e.g., register1 may be equal to the AND of register2 and register3 for all points in time. In such a situation, the register1 state variable is said to be redundant in view of register2 and register3.
The computations needed to verify a system design tend to become very expensive as the model being analyzed increases in complexity. Verification paradigms typically suffer exponential runtime with respect to the number of state elements of the design. By identifying the dependent state variables, the system model can be expressed with a fewer number of state elements, streamlining the formal verification paradigm. Identifying the dependent state variables is also useful in analyzing and enhancing circuit design, often resulting in reductions to circuit size for a particular application.
What is needed is an efficient way to identify dependent state variables and streamline the verification process. This disclosure introduces several mechanisms to enhance the speed and scalability of dependent state element identification.